es:ES, T:Type. strong-subtype(T;E)  (f:(TT). (x:T. f(x) c x)  retraction(T;f)) 

latex

Definitions

x:A  B(x), A c B, s = t, x:AB(x), P  Q, x:A. B(x), strong-subtype(A;B), ES, Type, E, t  T, b, f(a), <a, b>, EState(T), a:A fp B(a), Id, , EqDecider(T), Unit, left + right, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List, , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e', , constant_function(f;A;B), SWellFounded(R(x;y)), , pred!(e;e'), x,y. t(x;y), A, pred(e), first(e), x. t(x), P & Q, Top, let x,y = A in B(x;y), t.1, P  Q, P  Q, f(x)?z, e c e', (e < e'), retraction(T;f), P  Q, (x  l), x:A. B(x), {x:A| B(x)} , , |g|, S  T, a < b, Dec(P), A  B, b | a, a ~ b, a  b, a <p b, a < b, x f y, xL. P(x), (xL.P(x)), r < s, q-rel(r;x), Outcome, l_disjoint(T;l1;l2), False, Atom, {i..j}, x,y:A//B(x;y), |p|, |r|, , Atom$n, dstype(TypeNames; d; a), MaName, (e <loc e'), #$n, suptype(S; T), {T}

Lemmas

subtype rel function, le wf, decidable lt, es-causl-swellfnd, event system wf, strong-subtype wf, retraction wf, es-causl wf, es-causle wf, es-E wf, deq wf, EOrderAxioms wf, IdLnk wf, Msg wf, unit wf, nat wf, val-axiom wf, qle wf, cless wf, bool wf, top wf, Knd wf, kindcase wf, constant function wf, assert wf, not wf, loc wf, pred! wf, strongwellfounded wf, member wf, rationals wf, Id wf, EState wf, subtype rel wf